[Borralleras - PhD'03, Example 4.7.37]

Example 4.7.37 in [Borralleras - PhD'03]

Summary: Ex4_7_37_Bor03

CS-TRS format
OBJ format
Negative results:
Positive results:

CS-TRS Ex4_7_37_Bor03 (file Ex4_7_37_Bor03.csr)

Functions:  from cons s sel 0 minus quot zWquot nil

Constructors:  cons s 0 nil

Variables:  X XS N Y YS

Arities: 

ar(from) = 1
ar(cons) = 2
ar(s) = 1
ar(sel) = 2
ar(0) = 0
ar(minus) = 2
ar(quot) = 2
ar(zWquot) = 2
ar(nil) = 0

Replacement map: 

&181;(from)={1}
&181;(cons)={1}
&181;(s)={1}
&181;(sel)={1,2}
&181;(0)={}
&181;(minus)={1,2}
&181;(quot)={1,2}
&181;(zWquot)={1,2}
&181;(nil)={}

Rules: (file Ex4_7_37_Bor03)   

from(X) -> cons(X,from(s(X)))
sel(0,cons(X,XS)) -> X
sel(s(N),cons(X,XS)) -> sel(N,XS)
minus(X,0) -> 0
minus(s(X),s(Y)) -> minus(X,Y)
quot(0,s(Y)) -> 0
quot(s(X),s(Y)) -> s(quot(minus(X,Y),s(Y)))
zWquot(XS,nil) -> nil
zWquot(nil,XS) -> nil
zWquot(cons(X,XS),cons(Y,YS)) -> cons(quot(X,Y),zWquot(XS,YS))

The CS-TRS in OBJ format (file Ex4_7_37_Bor03.obj):

obj Ex4_7_37_Bor03 is
  sort S .
  op from : S -> S .
  op cons : S S -> S [strat (1 0)] .
  op s : S -> S .
  op sel : S S -> S .
  op 0 : -> S .
  op minus : S S -> S .
  op quot : S S -> S .
  op zWquot : S S -> S .
  op nil : -> S .
  vars X XS N Y YS : S .
  eq from(X) = cons(X,from(s(X))) .
  eq sel(0,cons(X,XS)) = X .
  eq sel(s(N),cons(X,XS)) = sel(N,XS) .
  eq minus(X,0) = 0 .
  eq minus(s(X),s(Y)) = minus(X,Y) .
  eq quot(0,s(Y)) = 0 .
  eq quot(s(X),s(Y)) = s(quot(minus(X,Y),s(Y))) .
  eq zWquot(XS,nil) = nil .
  eq zWquot(nil,XS) = nil .
  eq zWquot(cons(X,XS),cons(Y,YS)) = cons(quot(X,Y),zWquot(XS,YS)) .
endo

Negative results

The TRS is not simply mu-terminating [GL02b, Section 3]:
```
    quot(s(X),s(s(X))) -> s(quot(minus(X,s(X)),s(s(X))))
       ->_Emb^mu(F) quot(minus(X,s(X)),s(s(X)))
       ->_Emb^mu(F) quot(s(X),s(s(X)))
       -> ...
    
```
Therefore, by
[GL02b, Theorem 9], Ex4_7_37_Bor03 cannot be proved mu-terminating by using CSRPO (see also [Bor03, Example 4.7.37]) or Polynomials.

The µ-termination of Ex4_7_37_Bor03 cannot be proved by using Lucas' transformation: The TRS Ex4_7_37_Bor03_L:

    from(X) -> cons(X)
    sel(0,cons(X)) -> X
    sel(s(N),cons(X)) -> sel(N,XS)
    minus(X,0) -> 0
    minus(s(X),s(Y)) -> minus(X,Y)
    quot(0,s(Y)) -> 0
    quot(s(X),s(Y)) -> s(quot(minus(X,Y),s(Y)))
    zWquot(XS,nil) -> nil
    zWquot(nil,XS) -> nil
    zWquot(cons(X),cons(Y)) -> cons(quot(X,Y),zWquot(XS,YS))

contains extra variables.

Positive results

The µ-termination of Ex4_7_37_Bor03 is proved in [Bor03, Example 4.7.37] by using VCSMSPO together with the following:
- marking map:
```
	   m(cons,2)=m(_cons,2)={from,zWquot}
	   
```
- >=_Q = (>=_I,>^F_T)_lex with the precedence >=_F generated by
```
           quot >_F s
           
```
  and the interpretation generated by the pairs
```
           (minus(x,y),x); (quot(x,y),x)
	   
```
  and the identity for the rest of the symbols combined with CSRPO generated by the same marking map and the precedence >=_P defined by
```
	   from >_P cons, _from, s
	   sel >_P from, zWquot
	   zWquot >_P cons, _zWquot, from
	   
```
  with
```
           st(sel)=lex and 
           st(f)=mul for all other symbols f.
	   
```
By [GM04, Theorem 22], the µ-termination of Ex4_7_37_Bor03 can also be proved by using Giesl and Middeldorp's transformation (but no concrete proof has been reported yet).

The µ-termination of Ex4_7_37_Bor03 can also be proved by using Zantema's transformation. The TRS Ex4_7_37_Bor03_Z:

from(X) -> cons(X,n__from(s(X)))
sel(0,cons(X,XS)) -> X
sel(s(N),cons(X,XS)) -> sel(N,activate(XS))
minus(X,0) -> 0
minus(s(X),s(Y)) -> minus(X,Y)
quot(0,s(Y)) -> 0
quot(s(X),s(Y)) -> s(quot(minus(X,Y),s(Y)))
zWquot(XS,nil) -> nil
zWquot(nil,XS) -> nil
zWquot(cons(X,XS),cons(Y,YS)) -> cons(quot(X,Y),n__zWquot(activate(XS),activate(YS)))
from(X) -> n__from(X)
zWquot(X1,X2) -> n__zWquot(X1,X2)
activate(n__from(X)) -> from(X)
activate(n__zWquot(X1,X2)) -> zWquot(X1,X2)
activate(X) -> X

is terminating (use AProVE).